package Tracing;

import static org.w3c.dom.Node.COMMENT_NODE;
import static org.w3c.dom.Node.ELEMENT_NODE;
import static org.w3c.dom.Node.TEXT_NODE;
import java.util.Vector;
import java.util.regex.Matcher;
import java.util.regex.Pattern;

import javax.xml.parsers.DocumentBuilderFactory;
import javax.xml.parsers.ParserConfigurationException;

import org.w3c.dom.Attr;
import org.w3c.dom.Comment;
import org.w3c.dom.DOMException;
import org.w3c.dom.DOMImplementation;
import org.w3c.dom.Document;
import org.w3c.dom.Element;
import org.w3c.dom.NamedNodeMap;
import org.w3c.dom.Node;
import org.w3c.dom.NodeList;
import org.w3c.dom.Text;

import UI.Program;
import UI.TextPanePanel;
import UI.Utility;
import UI.View;

import prefuse.data.Graph;
import prefuse.data.Table;
import prefuse.data.Tree;
import prefuse.data.Tuple;

public class Trace {
	
	
	public Trace(){
		state = new State();
		
		historyStack = new HistoryStack();
		
		breakVariable = null;
		
		breakValue = null;
		
		breakLine = null;
		
		executeLine = null;
		
		hasErro = false;
		
		step = 1;
		
	}
	
	public Trace(View view){
		this();
		
		this.view = view;
		
		 //generate a table for detecting line numbers
		TextPanePanel sourcePanel = view.getSourcePanel();
		sourcePanel.setTable4Line(sourcePanel.getTable4LineNum());
		 for(int i = 0; i < sourcePanel.getTable4Line().getRowCount(); i++){
			 System.out.println(sourcePanel.getTable4Line().getString(i, "line")+":"+sourcePanel.getTable4Line().getString(i, "offset"));
		 }
		
		/*
		try {
			DOMImplementation domImpl = DocumentBuilderFactory.newInstance().newDocumentBuilder().getDOMImplementation();
			bufferDoc = domImpl.createDocument(null, "GTextbook", domImpl.createDocumentType("GTextbook", null,null));
		} catch(ParserConfigurationException e) {
			e.printStackTrace(System.err);
//			Display the error and terminate the current activity...
		} catch(DOMException e) {
			e.printStackTrace(System.err);
//		 	Determine the kind of error from the error code,
//		 	display the error, and terminate the current activity...
		}
*/
		
	}
	
	public Trace(Program program){
		this();
		/**
		 * tranversal the program to generate its history stack 
		 * according to the rules
		 */
		
		EnvironmentStack benvironment = new EnvironmentStack();
		
		SequentialExecute(program.getProgramRoot(), benvironment);
	
	}
	
	
	public Trace(Program program, View view){
		this(view);
		/**
		 * tranversal the program to generate its history stack 
		 * according to the rules one time
		 
		EnvironmentStack benvironment = new EnvironmentStack();
		
		SequentialExecute(program.getProgramRoot(), benvironment);
		*/
		
		this.currentTracingNode= program.getProgramRoot();
		this.currentBenvironment = new EnvironmentStack();
		
	
	}
	
	public String getExecuteLine() {
		return executeLine;
	}

	public void setExecuteLine(String executeLine) {
		this.executeLine = executeLine;
	}

	public HistoryStack getHistoryStack() {
		return historyStack;
	}


	public void setHistoryStack(HistoryStack historyStack) {
		this.historyStack = historyStack;
	}


	public State getState() {
		return state;
	}


	public void setState(State state) {
		this.state = state;
	}

	public String getBreakVariable() {
		return breakVariable;
	}

	public void setBreakVariable(String breakVariable) {
		this.breakVariable = breakVariable;
	}

	
	/*
	 * Execute the program sequentially
	 */
	public boolean SequentialExecute(Node block, EnvironmentStack benvironment){

			boolean result = true;
			NodeList list = block.getChildNodes();	
			if(list.getLength()>0){
				for(int i = 0; i < list.getLength(); i++){	
					Node currentNode = list.item(i);
					short type = currentNode.getNodeType();
					if(type == ELEMENT_NODE){
						EnvironmentStack currentBenvironment = benvironment.copy();
						result = execute(currentNode,currentBenvironment);
						/*
						 * print rules
						 */
						System.out.println("|\n|Rule(Block statement)\n|");
						view.getRulePanel().getTextArea().append("|\n|Rule(Block statement)\n|");
						if(!result){					
							break;
						}
					}
				}
			}
			
			return result;
	}
	//execute a single statement
	public boolean execute(Node node, EnvironmentStack benvironment){
		
		boolean result = true;
		
		//line number
		String lineNum = Utility.getAttr(node, "line");
		
		int type = statementType(node);
		//check the type of the clause
		
		/*if it is an assignment x:=..
		 * Rule 3.1
		 */
		if(type == assignment){
			String clause = null;
			NodeList list = node.getChildNodes();	
			if(list.getLength()>0){
				for(int i = 0; i < list.getLength(); i++){	
						Node currentNode = list.item(i);
						clause = ((Text)currentNode).getTextContent();
				}
			}
			
			
			
			//parse the assignment clause	
			Vector<String> str = Utility.getItemsBySeparator(clause,":=");
			
			
			//parse the expected state
			State expectedState = new State();
			
			String Estate = Utility.getAttr(node, "Estate");
			if(Estate!=null){
				Vector<String> states = Utility.getItemsBySeparator(Estate,";");
				for(int j = 0; j < states.size(); j++){
					Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
					expectedState.set(Estr.get(0), Estr.get(1));
				}
			}
			
			historyStack.push(str.get(0), str.get(1), state.copy(), expectedState, benvironment, lineNum);
			
			System.out.println("|\n|Rule(Assign statement)\n|");
			view.getRulePanel().getTextArea().append("|\n|Rule(Assign statement)\n|");
			
			historyStack.print();
			historyStack.print(view);
			
			state.transform(str.get(0),str.get(1));
			
			/*
			 * terminate point
			 */
			Tuple breaktuple = state.compareWith(expectedState);
			if(breaktuple!=null){
				//System.out.println(breaktuple.get("variable"));
				breakVariable = (String)breaktuple.get("variable");
				breakValue = (String)breaktuple.get("value");
				breakLine = lineNum;
				result = false;
				System.out.println("|\n|"+breakVariable+"="+breakValue+" at line " + lineNum +": Rule(Termination)\n|");
				view.getRulePanel().getTextArea().append("|\n|"+breakVariable+"="+breakValue+" at line " + lineNum +": Rule(Termination)\n|");

			}
		}
			
			
		/*if it is if clause
		 * condition is true  ---- Rule 3.4
		 * condition is false ---- Rule 3.5	
		 */
		
		if(type == ifStatement){

			String condition = Utility.getAttr(node, "condition");
			
			//parse the expected state
			State expectedState = new State();
			String Estate = Utility.getAttr(node, "Estate");
			if(Estate!=null){
				Vector<String> states = Utility.getItemsBySeparator(Estate,";");
				for(int j = 0; j < states.size(); j++){
					Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
					expectedState.set(Estr.get(0), Estr.get(1));
				}
			}
			
			String expectedvalue = Utility.getAttr(node, "Evalue");
			
			String evalCondition = state.execute(condition);
			
			//state.print();
			//System.out.println(evalCondition);
				
			if(evalCondition.equals("1.0")){
				/*
				 * 
				 */
				System.out.println("|\n|Rule if true\n|");
				view.getRulePanel().getTextArea().append("|\n|Rule if true\n|");

				benvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
				benvironment.print();
				benvironment.print(view);
				
				Node currentNode = Utility.getChildById(node, 1, ELEMENT_NODE);
				if(currentNode!=null){
					result = SequentialExecute(currentNode,benvironment);
				}
			}else{
				System.out.println("|\n|Rule if false\n|");
				view.getRulePanel().getTextArea().append("|\n|Rule if false\n|");
				
				benvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
				benvironment.print();
				benvironment.print(view);
				Node currentNode = Utility.getChildById(node, 2, ELEMENT_NODE);
				if(currentNode!=null){
					result = SequentialExecute(currentNode,benvironment);		
				}
			
			}
			
			
		}
		
		if(type == whileStatement){
			
			//parse the expected state
			State expectedState = new State();
			String Estate = Utility.getAttr(node, "Estate");
			if(Estate!=null){
				Vector<String> states = Utility.getItemsBySeparator(Estate,";");
				for(int j = 0; j < states.size(); j++){
					Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
					expectedState.set(Estr.get(0), Estr.get(1));
				}
			}
			
			String expectedvalue = Utility.getAttr(node, "Evalue");
			String condition = Utility.getAttr(node, "condition");
			String evalCondition = state.execute(condition);
			
			if(evalCondition.equals("1.0")){
				System.out.println("|\n|Rule while true\n|");
				view.getRulePanel().getTextArea().append("|\n|Rule while true\n|");
				benvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
				benvironment.print();
				benvironment.print(view);
				
				Node currentNode = Utility.getChildById(node, 1, ELEMENT_NODE);
				if(currentNode!=null){
					result = SequentialExecute(currentNode,benvironment);
				}
				//the body of while has no error
				if(result == true){
					result = execute(node,benvironment);
				}	
			}else{
				System.out.println("|\n|Rule while false\n|");
				view.getRulePanel().getTextArea().append("|\n|Rule while true\n|");
			}
		}
		
		return result;

	}		
		
	//execute a single statement
	public void executeStepByStep(Node node){
		
		
		//line number
		String lineNum = Utility.getAttr(node, "line");
		
		int type = statementType(node);
		//check the type of the clause
		
		if(type == sequence||type == block){
			Node n = Utility.getChildById(node, 1, ELEMENT_NODE);
			if(n!=null){
				this.setCurrentTracingNode(n);
				executeStepByStep(n);
			}
		}else{
		
			view.getRulePanel().getTextArea().append("Tracing step "+ step++ + ":\n");
		
		
			/*if it is an assignment x:=..
			 * Rule 3.1
			 */
			if(type == assignment){
				String clause = null;
				NodeList list = node.getChildNodes();	
				if(list.getLength()>0){
					for(int i = 0; i < list.getLength(); i++){	
						Node currentNode = list.item(i);
						clause = ((Text)currentNode).getTextContent();
					}
				}
			
			
			
				//parse the assignment clause	
				Vector<String> str = Utility.getItemsBySeparator(clause,":=");
			
			
				//parse the expected state
				State expectedState = new State();
			
				String Estate = Utility.getAttr(node, "Estate");
				if(Estate!=null){
					Vector<String> states = Utility.getItemsBySeparator(Estate,";");
					for(int j = 0; j < states.size(); j++){
						Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
						expectedState.set(Estr.get(0), Estr.get(1));
					}
				}
			
				oldState = state.copy();
			
				historyStack.push(str.get(0), str.get(1), oldState, expectedState, currentBenvironment.copy(), lineNum);
				historyStack.print();
				historyStack.print(view);
				state.transform(str.get(0),str.get(1));
			
			
				System.out.println("|\n|Rule(Assign statement)\n|");
				view.getRulePanel().getTextArea().append(Utility.getAssignmentTracingRule(str.get(1), oldState, state.copy(), state.getValue(str.get(0)), str.get(0)));
			
				/*
				 * terminate point
				 */
				Tuple breaktuple = state.compareWith(expectedState);
				if(breaktuple!=null){
					//System.out.println(breaktuple.get("variable"));
					breakVariable = (String)breaktuple.get("variable");
					breakValue = (String)breaktuple.get("value");
					breakLine = lineNum;
					expectedTerminationState = expectedState;
					this.setHasErro(true);
					System.out.println("|\n|"+breakVariable+"="+breakValue+" at line " + lineNum +": Rule(Termination)\n|");
					view.getRulePanel().getTextArea().append(Utility.getTerminationTracingRule(state.getValue(str.get(0)), breakValue, clause, oldState));
					this.setCurrentTracingNode(null);
				}else{
					//set the next tracing node
					this.setCurrentTracingNode(this.getNextTracingNode(this.currentTracingNode));
				
				}
			}
			
			
			/*if it is if clause
			 * condition is true  ---- Rule 3.4
			 * condition is false ---- Rule 3.5	
			 */
		
			if(type == ifStatement){
				String condition = Utility.getAttr(node, "condition");
			
				//parse the expected state
				State expectedState = new State();
				String Estate = Utility.getAttr(node, "Estate");
				if(Estate!=null){
					Vector<String> states = Utility.getItemsBySeparator(Estate,";");
					for(int j = 0; j < states.size(); j++){
						Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
						expectedState.set(Estr.get(0), Estr.get(1));
					}
				}
			
				String expectedvalue = Utility.getAttr(node, "Evalue");
				
				String evalCondition = state.execute(condition);
			
				//state.print();
				//System.out.println(evalCondition);
				
				if(evalCondition.equals("1.0")){
					/*
					 * 
					 */
					System.out.println("|\n|Rule if true\n|");
					view.getRulePanel().getTextArea().append(Utility.getIfTrueStatementTracingRule(condition, state));

					currentBenvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
					currentBenvironment.print();
					currentBenvironment.print(view);
				
					this.setCurrentTracingNode(Utility.getChildById(node, 1, ELEMENT_NODE));
				}else{
					System.out.println("|\n|Rule if false\n|");
					view.getRulePanel().getTextArea().append(Utility.getIfFalseStatementTracingRule(condition, state));
				
					currentBenvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
					currentBenvironment.print();
					currentBenvironment.print(view);

					this.setCurrentTracingNode(Utility.getChildById(node, 2, ELEMENT_NODE));
				}
			}
		
			if(type == whileStatement){
			
				//parse the expected state
				State expectedState = new State();
				String Estate = Utility.getAttr(node, "Estate");
				if(Estate!=null){
					Vector<String> states = Utility.getItemsBySeparator(Estate,";");
					for(int j = 0; j < states.size(); j++){
						Vector<String> Estr = Utility.getItemsBySeparator(states.get(j),"=");
						expectedState.set(Estr.get(0), Estr.get(1));
					}
				}
			
				String expectedvalue = Utility.getAttr(node, "Evalue");
				String condition = Utility.getAttr(node, "condition");
				String evalCondition = state.execute(condition);
				
				if(evalCondition.equals("1.0")){
					System.out.println("|\n|Rule while true\n|");
					view.getRulePanel().getTextArea().append(Utility.getWhileTrueStatementTracingRule(condition, state));
					currentBenvironment.push(condition, state.copy(), expectedState, expectedvalue, lineNum);
					currentBenvironment.copy().print();
					currentBenvironment.copy().print(view);
					this.setCurrentTracingNode(Utility.getChildById(node, 1, ELEMENT_NODE));	
				}else{
					System.out.println("|\n|Rule while false\n|");
					view.getRulePanel().getTextArea().append(Utility.getWhileFalseStatementTracingRule(condition, state));
					this.setCurrentTracingNode(this.getNextTracingNode(this.getCurrentTracingNode()));
				}
				
			}
			if(lineNum!=null){
				this.executeLine = lineNum;
			}
		}
	}
	
	
	
	public State getExpectedTerminationState() {
		return expectedTerminationState;
	}

	public void setExpectedTerminationState(State expectedTerminationState) {
		this.expectedTerminationState = expectedTerminationState;
	}

	public Node getNextTracingNode(Node current){
		Node next = null;
		String currentStatement = "S";
		String nextStatement = "S'";
		if(current.getNodeName().equals("assignment")){
			currentStatement = ((Text)current.getChildNodes().item(0)).getTextContent();
		}else
			if(current.getNodeName().equals("if")){
				currentStatement = "if(" + Utility.getAttr(current, "condition") + ")";
			}else
				if(current.getNodeName().equals("while")){
					currentStatement = "while(" + Utility.getAttr(current, "condition") + ")";
				}
		Node currentParent = current.getParentNode();
		if(currentParent!=null){
			if(currentParent.getNodeName().equals("sequence")){
				next = Utility.getNextNode(current, ELEMENT_NODE);
				if(next!=null){
					System.out.println("|\n|Sequential statement Rule\n|");
					if(next.getNodeName().equals("assignment")){
						nextStatement = ((Text)next.getChildNodes().item(0)).getTextContent();
					}else
						if(next.getNodeName().equals("if")){
							nextStatement = "if(" + Utility.getAttr(next, "condition") + ")";
						}else
							if(next.getNodeName().equals("while")){
								nextStatement = "while(" + Utility.getAttr(next, "condition") + ")";
							}
					view.getRulePanel().getTextArea().append(Utility.getSequenceTracingRule(currentStatement,nextStatement,oldState, state));
				}
			}else
				if(currentParent.getNodeName().equals("block")){
					next = Utility.getNextNode(current, ELEMENT_NODE);
					if(next == null){
						currentBenvironment.pop();
						if(statementType(currentParent.getParentNode())==ifStatement){
							next = getNextTracingNode(currentParent.getParentNode());
						}else
							if(statementType(currentParent.getParentNode())==whileStatement){
								next = currentParent.getParentNode();
							}
						System.out.println("|\n|Block statement Rule\n|");
						view.getRulePanel().getTextArea().append(Utility.getBlockTracingRule(currentStatement,oldState, state));
					}
				}
		}
		
		
		return next;
	}
	
	public String getBreakLine() {
		return breakLine;
	}

	public void setBreakLine(String breakLine) {
		this.breakLine = breakLine;
	}

	public String getBreakValue() {
		return breakValue;
	}

	public void setBreakValue(String breakValue) {
		this.breakValue = breakValue;
	}

	public int statementType(Node node){
		int type = -1;
		short nodeType = node.getNodeType();
		if(nodeType == ELEMENT_NODE){
			String name =  node.getNodeName();
			if(name.equals("block")){
				type = block;
			}else
				if(name.equals("sequence")){
					type = sequence;
				}else
			if(name.equals("assignment")){
				type = assignment;
			}else
			if(name.equals("if")){
				type = ifStatement;
			}else
			if(name.equals("while")){
				type = whileStatement;
			}
		}
		
		
		return type;
	}
	

	
	private HistoryStack historyStack;
	private State state, oldState;
	private String breakVariable;
	private String breakValue;
	private String breakLine;
	private String executeLine;
	private View view;
	private Node currentTracingNode;
	private EnvironmentStack currentBenvironment;
	private boolean hasErro;
	private int step;
	private State expectedTerminationState;

	public boolean isHasErro() {
		return hasErro;
	}

	public void setHasErro(boolean hasErro) {
		this.hasErro = hasErro;
	}

	public Node getCurrentTracingNode() {
		return currentTracingNode;
	}

	public void setCurrentTracingNode(Node currentTracingNode) {
		this.currentTracingNode = currentTracingNode;
	}

	public View getView() {
		return view;
	}

	public void setView(View view) {
		this.view = view;
	}



	//private Document bufferDoc;
	private static int sequence = 0;
	private static int block = 1;
	private static int assignment = 2;
	private static int ifStatement = 3;
	private static int whileStatement = 4;
	
	

}
